Nuprl Lemma : idlnk-deq_wf
0,22
postcript
pdf
IdLnkDeq
EqDecider(IdLnk)
latex
Definitions
IdDeq
,
t
T
,
Id
,
x
:
A
.
B
(
x
)
,
product-deq(
A
;
B
;
a
;
b
)
,
x
:
A
B
(
x
)
,
IdLnkDeq
,
IdLnk
Lemmas
product-deq
wf
,
Id
wf
,
id-deq
wf
origin
EqDecider(IdLnk) EqDecider(IdLnk) T
x:A. B(x)
B(x)